Formal Specification and Validation of Security Policies
Identifieur interne : 001E34 ( Main/Exploration ); précédent : 001E33; suivant : 001E35Formal Specification and Validation of Security Policies
Auteurs : Tony Bourdier [France] ; Horatiu Cirstea [France] ; Mathieu Jaume [France] ; Hélène Kirchner [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
English descriptors
Abstract
Abstract: We propose a formal framework for the specification and validation of security policies. To model a secured system, the evolution of security information in the system is described by transitions triggered by authorization requests and the policy is given by a set of rules describing the way the corresponding decisions are taken. Policy rules are constrained rewrite rules whose constraints are first-order formulas on finite domains, which provides enhanced expressive power compared to classical security policy specification approaches like the ones using Datalog, for example. Our specifications have an operational semantics based on transition and rewriting systems and are thus executable. This framework also provides a common formalism to define, compare and compose security systems and policies. We define transformations over secured systems in order to perform validation of classical security properties.
Url:
DOI: 10.1007/978-3-642-27901-0_12
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003C93
- to stream Istex, to step Curation: 003C49
- to stream Istex, to step Checkpoint: 000423
- to stream Hal, to step Corpus: 002380
- to stream Hal, to step Curation: 002380
- to stream Hal, to step Checkpoint: 001E47
- to stream Main, to step Merge: 001E53
- to stream Main, to step Curation: 001E34
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Formal Specification and Validation of Security Policies</title><author><name sortKey="Bourdier, Tony" sort="Bourdier, Tony" uniqKey="Bourdier T" first="Tony" last="Bourdier">Tony Bourdier</name></author><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name></author><author><name sortKey="Jaume, Mathieu" sort="Jaume, Mathieu" uniqKey="Jaume M" first="Mathieu" last="Jaume">Mathieu Jaume</name></author><author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FDF9E7EE581060E3608FE75B2DCD930CDB3A8170</idno><date when="2012" year="2012">2012</date><idno type="doi">10.1007/978-3-642-27901-0_12</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-05C4WRNR-Z/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C93</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C93</idno><idno type="wicri:Area/Istex/Curation">003C49</idno><idno type="wicri:Area/Istex/Checkpoint">000423</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000423</idno><idno type="wicri:doubleKey">0302-9743:2012:Bourdier T:formal:specification:and</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00507300</idno><idno type="url">https://hal.inria.fr/inria-00507300</idno><idno type="wicri:Area/Hal/Corpus">002380</idno><idno type="wicri:Area/Hal/Curation">002380</idno><idno type="wicri:Area/Hal/Checkpoint">001E47</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">001E47</idno><idno type="wicri:Area/Main/Merge">001E53</idno><idno type="wicri:Area/Main/Curation">001E34</idno><idno type="wicri:Area/Main/Exploration">001E34</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Formal Specification and Validation of Security Policies</title><author><name sortKey="Bourdier, Tony" sort="Bourdier, Tony" uniqKey="Bourdier T" first="Tony" last="Bourdier">Tony Bourdier</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>INRIA Nancy - Grand-Est Research Center & Nancy-Université & LORIA</wicri:regionArea></affiliation></author><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>INRIA Nancy - Grand-Est Research Center & Nancy-Université & LORIA</wicri:regionArea></affiliation></author><author><name sortKey="Jaume, Mathieu" sort="Jaume, Mathieu" uniqKey="Jaume M" first="Mathieu" last="Jaume">Mathieu Jaume</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>SPI LIP6, Université Paris 6</wicri:regionArea><wicri:noRegion>Université Paris 6</wicri:noRegion><wicri:noRegion>Université Paris 6</wicri:noRegion></affiliation></author><author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>INRIA Bordeaux - Sud-Ouest Research Center</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Security policies</term><term>constrained rewriting systems</term><term>formal specification</term><term>formal validation</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We propose a formal framework for the specification and validation of security policies. To model a secured system, the evolution of security information in the system is described by transitions triggered by authorization requests and the policy is given by a set of rules describing the way the corresponding decisions are taken. Policy rules are constrained rewrite rules whose constraints are first-order formulas on finite domains, which provides enhanced expressive power compared to classical security policy specification approaches like the ones using Datalog, for example. Our specifications have an operational semantics based on transition and rewriting systems and are thus executable. This framework also provides a common formalism to define, compare and compose security systems and policies. We define transformations over secured systems in order to perform validation of classical security properties.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Bourdier, Tony" sort="Bourdier, Tony" uniqKey="Bourdier T" first="Tony" last="Bourdier">Tony Bourdier</name></noRegion><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name><name sortKey="Jaume, Mathieu" sort="Jaume, Mathieu" uniqKey="Jaume M" first="Mathieu" last="Jaume">Mathieu Jaume</name><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001E34 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001E34 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:FDF9E7EE581060E3608FE75B2DCD930CDB3A8170
|texte= Formal Specification and Validation of Security Policies
}}
| This area was generated with Dilib version V0.6.33. |  |